FDL - Nuprl Lemma : strict-sorted

Nuprl Lemma : strict-sorted

T:Type.
T

(

as:T List. sorted(as) & no_repeats(T;as)

(

i:

||as||, j:

i. as[j]<as[i]))

Definitions t T, x:A. B(x), ||as||, P & Q, i j < k, P Q, False, A, AB, {i..j}, S T, l[i], no_repeats(T;l), sorted(L), Prop, P Q, P Q, ij, , {T}, SQType(T), P Q, Dec(P)

Lemmas not wf, nat wf, decidable lt, le wf, sorted wf, no repeats wf, int seg wf, select wf, length wf1